Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Added model classes for java.nio.file and java.nio.charset packages #429 #506

Merged
merged 4 commits into from
Dec 15, 2024
Merged

Added model classes for java.nio.file and java.nio.charset packages #429 #506

merged 4 commits into from
Dec 15, 2024

Conversation

joalen
Copy link
Contributor

@joalen joalen commented Nov 17, 2024

Turns out, there needs to be new model classes found in the java.nio.charset and java.nio.file packages. I believe I made them as small as I could to patch the issue with the original reproducer.

The following happens when this new solution works:

JavaPathfinder core system v8.0 (rev 8fe399b8718b1a25055f18b61707ca0cf03112f0) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
BoundedBuffer.main()

====================================================== search started: 11/16/24, 10:42 PM

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=1,visited=0,backtracked=1,end=1
search:             maxDepth=1,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap:               new=555,released=35,maxLive=0,gcCycles=1
instructions:       9557
max memory:         2056MB
loaded code:        classes=93,methods=2360

====================================================== search finished: 11/16/24, 10:42 PM```

@joalen
Found Potential Fix for javapathfinder#429
d48e34d 
Seems like there needs to be model classes in the file and charset packages for java.nio. These are as small as I could make them
@joalen
Create NullCharsetTest.java
1ee4a1a 
Developed UnitTest to address the error from javapathfinder#429
@joalen
Update NullCharsetTest.java
c27a20a 
Should be "iae" and not "e"
@cyrille-artho
Copy link
Member

Thank you for your contribution. When running the test cases, four tests fail. This is probably because your model classes replace built-in library classes and their behavior is not totally consistent.
Could you please look into this? Perhaps some model classes can be removed, or they have to be amended to make the existing test cases pass. Occasionally, a test case is too strict or specific.

@joalen
Fixed Failing Tests for NullCharSet
11cf430 
It turns out my implementation of Charset affected the behavior of underlying Gradle JPF tests. Removed this custom Charset implementation and instead kept four files to fix the root cause:
 - FileSystem.java
 - FileSystems.java
 - Pathy.java
 - spi/FileSystemProvider.java

All other files in the initial commit to PR were redundant.
@joalen
Copy link
Contributor Author

joalen commented Dec 15, 2024

@cyrille-artho

Yep, seems like there were some redundant classes and Charset caused issues with the current JPF pipeline. I created a new commit to address some of the issues and it should now work. Thank you again for catching that!!

@cyrille-artho
Copy link
Member

Thanks, with this, we have a few classes less to maintain, and the tests pass.

@cyrille-artho cyrille-artho merged commit ca40e6c into javapathfinder:master Dec 15, 2024
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@joalen @cyrille-artho